//CWE-1224 
/*
Consider the example design module system verilog code shown below. register_write_once_example module is an example of register that has a write-once field defined. Bit 0 field captures the write_once_status value. This implementation can be for a register that is defined by specification to be a write-once register, since the write_once_status field gets written by input data bit 0 on first write.
The above example only locks further writes if write_once_status bit is written to one. So it acts as write_1-Once instead of the write-once attribute.
*/
module register_write_once_example
(
input [15:0] Data_in,
input Clk,
input ip_resetn,
input global_resetn,
input write,
output reg [15:0] Data_out
);

reg Write_once_status;

always @(posedge Clk or negedge ip_resetn)
if (~ip_resetn)
begin
Data_out <= 16'h0000;
Write_once_status <= 1'b0;
end
else if (write & ~Write_once_status)
begin
Data_out <= Data_in & 16'hFFFE;
Write_once_status <= Data_in[0]; // Input bit 0 sets Write_once_status
//Write_once_status <= 1'b1;
end
else if (~write)
begin
Data_out[15:1] <= Data_out[15:1];
Data_out[0] <= Write_once_status;
end

initial assume(~ip_resetn);
// always @(posedge Clk)
// if($past(ip_resetn) &&ip_resetn &&$past(write) && $past(~Write_once_status))begin
//     assert(Write_once_status==1'b1);
// end
always @(posedge Clk)
if($past(ip_resetn,2) && $past(ip_resetn) && ip_resetn && $past(write,2) && $past(~Write_once_status,2))begin
    assert(Data_out[15:1] == $past(Data_out[15:1]));
end
endmodule